(declare-const v0 Bool)
(declare-const v1 Bool)
(declare-const v2 Bool)
(declare-const r1 Real)
(declare-const r2 Real)
(declare-const r3 Real)
(declare-const r4 Real)
(declare-const r6 Real)
(declare-const r8 Real)
(declare-const r9 Real)
(declare-const v3 Bool)
(declare-const r10 Real)
(declare-const v4 Bool)
(declare-const v5 Bool)
(declare-const v6 Bool)
(declare-const r11 Real)
(assert (or v6 v3 (= r1 (- r8) r1)))
(assert (or (= (/ r2 1146551.0) r1 r1) (= (/ r2 1146551.0) r1 r1) (and (= (/ r2 1146551.0) r1 r1) v0 v0)))
(assert (or v6 v2 (=> (xor v1 v0 v3 v0 v2 v2) v1)))
(assert (or (=> (xor v1 v0 v3 v0 v2 v2) v1) (=> (xor v1 v0 v3 v0 v2 v2) v1) (and (= (/ r2 1146551.0) r1 r1) v0 v0)))
(assert (or (not v3) v1 v3))
(assert (or (not v3) v0 (> r10 r4 (/ r2 1146551.0) r4)))
(assert (or (and (= (/ r2 1146551.0) r1 r1) v0 v0) v0 v1))
(assert (or (=> (xor v1 v0 v3 v0 v2 v2) v1) v1 (not v3)))
(assert (or v4 v6 (=> (xor v1 v0 v3 v0 v2 v2) v1)))
(assert (or v0 (= r1 (- r8) r1) (=> (xor v1 v0 v3 v0 v2 v2) v1)))
(check-sat)
